package simplytypeddebruijn

/**
   * Following typechecking as in Types and Programming Languages by Benjamin Pierce, chap 9-10-11
   *
   */

trait SimplyTypedTypeCheck extends TypeChecker {self: TypeChecker with PrettyPrinter with AbstractSyntax =>
  case class VarBinding(ltype: LType) extends Binding 

  def typeOf(t:LTerm)  = Typer.fresh.typeOf(t)

  object Typer {
    def fresh() = new SystemFTyperFun { val ctx = new StringBindingContext[VarBinding](Nil) }
  }

  trait Typer extends Function1[LTerm, LType] {
    
    type Ctx = StringBindingContext[VarBinding]
    val ctx: Ctx

    def rememberingTypeOfVar(str: String, ty: LType) = {
      val ctxextended = ctx + (str, VarBinding(ty))
      create(ctxextended)
    }
    def recallTypeOfVar(offset:Int) = ctx(offset) match {
      case Some(VarBinding(ty)) => ty
      case None                 => throw new TypeExc("no varbinding found for variable with offset "+offset)
    }
    
    //def lookupVar(n: Int) = ctx(n)
    //def removingBinder(ty:LType) = ty

    def apply(t:LTerm):LType = { typeOf(t) }

    def typeOf(t: LTerm): LType
    def create(ctx: Ctx): Typer
  }

  
  
  
  trait SystemFTyperFun extends Typer {
    def create(initctx: Ctx)= {
      new SystemFTyperFun {val ctx = initctx}
    }
    def typeOf(t: LTerm)= t match {
         
      case Lit(n)     => TyInt
      case Tru()      => TyBool
      case Fls()      => TyBool 
      case Unit()     => TyUnit
        
        case If(cond,pos,neg) => {
           if (TyBool != typeOf(cond)) throw new TypeExc("conditional not boolean")
           val typpos = typeOf(pos)
           if ( typpos != typeOf(neg)) throw new TypeExc("branches of if differ in type: "+prettyPrint(typeOf(pos))+" vs "+prettyPrint(typeOf(neg)))
           typpos
        }


        
        
        case Let(hint,conc,body) => {
          val typeInsert = typeOf(conc)
          rememberingTypeOfVar(hint, typeInsert).typeOf(body)
        }
        
        case Var(n)       =>   { //T-Var
          recallTypeOfVar(n)
        }
        
        
        case Lam(hint,ty,body) => {  //T-Abs
           TyArr(ty, rememberingTypeOfVar(hint,ty).typeOf(body))
        }
        case App(tfun,targ)  => {  //T-App
          val funty = typeOf(tfun)
          val argty = typeOf(targ)
          funty match {
            case TyArr(fundom, funrange) => {
              //concrete and formal parameter types need to match
              if  (argty == fundom ) funrange 
              else throw new TypeExc("wrong application argument type: receive "+ (if(argty==null) "untyped" else prettyPrint(argty)) 
                +" but expect "+ (if(fundom==null)"" else prettyPrint(fundom) )+ " \n at "+prettyPrint(t))
             }
             case _ => throw new TypeExc("applying to non function type: arg ="+prettyPrint(targ)+" non-func ="+prettyPrint(tfun))
          }
        }
        
        
        case r@Record(fields)       => { 
          TyRecord(r.fieldsmap(typeOf))
       }
       case RecProj(t,label) => {
       typeOf(t) match {
         case r@TyRecord(fields) =>
              r.field(label)
         case _         => throw new TypeExc("trying to project field "+label+" of non-record:"+prettyPrint(t))
       }
       
       }
        
   }
  
  }
    
    
}

